b:, f:(b). (n:b. f(n))  mu(f)  b 

latex

Definitions	T, True, Dec(P), P  Q, SQType(T), {T}, ij, Unit, P  Q, x:A. B(x), , , Prop, b, b, t  T, x:A. B(x), i  j < k, AB, P & Q, A, False, P  Q, {i..j}, mu(f)
Lemmas	assert wf, not wf, bnot wf, bool wf, le wf, nat wf, mu wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, int seg wf, nat properties, ge wf, decidable int equal, true wf, squash wf